(set-logic QF_BV)
(declare-fun x () (_ BitVec 9))
(declare-fun b1 () Bool)
(declare-fun b2 () Bool)
(declare-fun b3 () Bool)
(define-fun f924 () (_ BitVec 9) (ite (and (not b3) b1) (_ bv8448 9) x))
(define-fun f935 () (_ BitVec 9) (ite (and (not b3) b1) (_ bv8482 9) (_ bv0 9)))
(assert (not (= f924 (_ bv8656 9))))
(define-fun f1906 () (_ BitVec 9) (ite b2 f935 (_ bv0 9)))
(assert (= f1906 (_ bv0 9)))
(check-sat)
(exit)
